/**
 * Provides classes representing control flow completions.
 *
 * A completion represents how a statement or expression terminates.
 */

private import swift
private import codeql.swift.controlflow.ControlFlowGraph
private import ControlFlowElements
private import ControlFlowGraphImpl

private newtype TCompletion =
  TSimpleCompletion() or
  TBooleanCompletion(boolean b) { b in [false, true] } or
  TBreakCompletion(Stmt target) { target = any(BreakStmt stmt).getTarget() } or
  TContinueCompletion(Stmts::Loops::LoopStmt target) { target = any(ContinueStmt stmt).getTarget() } or
  TReturnCompletion() or
  TMatchingCompletion(boolean isMatch) { isMatch in [false, true] } or
  TFallthroughCompletion(CaseStmt dest) { dest = any(FallthroughStmt stmt).getFallthroughDest() } or
  TEmptinessCompletion(boolean isEmpty) { isEmpty in [false, true] } or
  TThrowCompletion()

/** Holds if `c` is a valid completion after evaluating `stmt`. */
pragma[noinline]
private predicate completionIsValidForStmt(Stmt stmt, Completion c) {
  c = TBreakCompletion(stmt.(BreakStmt).getTarget())
  or
  c = TContinueCompletion(stmt.(ContinueStmt).getTarget())
  or
  (
    // Exclude return completions from returns that are implicit generated by an autoclosure expression.
    stmt instanceof ReturnStmt and not stmt = any(AutoClosureExpr closure).getReturn()
    or
    // `FailStmt` is only emitted in place of `return nil` in failable initializers.
    stmt instanceof FailStmt
  ) and
  c = TReturnCompletion()
  or
  c = TFallthroughCompletion(stmt.(FallthroughStmt).getFallthroughDest())
}

/** A completion of a statement or an expression. */
abstract class Completion extends TCompletion {
  private predicate isValidForSpecific(ControlFlowElement n) {
    completionIsValidForStmt(n.asAstNode(), this)
    or
    mustHaveBooleanCompletion(n) and
    (
      exists(boolean value | isBooleanConstant(n, value) | this = TBooleanCompletion(value))
      or
      not isBooleanConstant(n, _) and
      this = TBooleanCompletion(_)
    )
    or
    mustHaveMatchingCompletion(n.asAstNode()) and
    (
      exists(boolean value | isMatchingConstant(n.asAstNode(), value) |
        this = TMatchingCompletion(value)
      )
      or
      not isMatchingConstant(n.asAstNode(), _) and
      this = TMatchingCompletion(_)
    )
    or
    mustHaveThrowCompletion(n.asAstNode(), this)
  }

  /** Holds if this completion is valid for node `n`. */
  predicate isValidFor(ControlFlowElement n) {
    this.isValidForSpecific(n)
    or
    this instanceof ThrowCompletion and
    mayHaveThrowCompletion(n)
    or
    not any(Completion c).isValidForSpecific(n) and
    this = TSimpleCompletion()
  }

  /**
   * Holds if this completion will continue the loop `stmt` when it is the completion
   * of a loop body.
   */
  predicate continuesLoop(Stmts::Loops::LoopStmt stmt) { none() }

  /** Gets a successor type that matches this completion. */
  abstract SuccessorType getAMatchingSuccessorType();

  /** Gets a textual representation of this completion. */
  abstract string toString();
}

/** Holds if node `n` has the Boolean constant value `value`. */
private predicate isBooleanConstant(ControlFlowElement n, boolean value) {
  mustHaveBooleanCompletion(n) and
  value = n.asAstNode().(BooleanLiteralExpr).getValue()
  or
  // Boolean constants hidden inside conversions are also
  // constants that resolve to the same value.
  exists(ControlFlowElement parent |
    parent.asAstNode() = n.asAstNode().getResolveStep() and
    isBooleanConstant(parent, value)
  )
}

/**
 * Holds if a normal completion of `n` must be a Boolean completion.
 */
private predicate mustHaveBooleanCompletion(ControlFlowElement n) { inBooleanContext(n) }

/**
 * Holds if `n` is used in a Boolean context. That is, the value
 * that `n` evaluates to determines a true/false branch successor.
 */
private predicate inBooleanContext(ControlFlowElement n) {
  astInBooleanContext(n.asAstNode()) or
  astInBooleanContext(n.(PropertyGetterElement).getRef()) or
  astInBooleanContext(n.(PropertySetterElement).getAssignExpr()) or
  astInBooleanContext(n.(PropertyObserverElement).getAssignExpr())
}

private predicate astInBooleanContext(AstNode n) {
  n = any(ConditionElement condElem).getBoolean().getFullyUnresolved()
  or
  n = any(ConditionElement condElem).getAvailability().getFullyUnresolved()
  or
  n = any(StmtCondition stmtCond).getFullyUnresolved()
  or
  exists(RepeatWhileStmt repeat | n = repeat.getCondition().getFullyConverted())
  or
  exists(LogicalAndExpr parent |
    n = parent.getLeftOperand().getFullyConverted()
    or
    astInBooleanContext(parent) and
    n = parent.getRightOperand().getFullyConverted()
  )
  or
  exists(LogicalOrExpr parent |
    n = parent.getLeftOperand().getFullyConverted()
    or
    astInBooleanContext(parent) and
    n = parent.getRightOperand().getFullyConverted()
  )
  or
  n = any(NotExpr parent | astInBooleanContext(parent)).getOperand().getFullyConverted()
  or
  exists(IfExpr ifExpr |
    ifExpr.getCondition().getFullyConverted() = n
    or
    astInBooleanContext(ifExpr) and
    n = ifExpr.getBranch(_).getFullyConverted()
  )
  or
  exists(ForEachStmt foreach | n = foreach.getWhere().getFullyConverted())
  or
  exists(Exprs::Conversions::ConversionOrIdentityTree parent |
    astInBooleanContext(parent.getAst()) and
    parent.convertsFrom(n)
  )
}

/**
 * Holds if a normal completion of `ast` must be a matching completion. Thats is,
 * whether `ast` determines a match in a `switch` or `catch` statement.
 */
private predicate mustHaveMatchingCompletion(AstNode ast) { ast instanceof Pattern }

/**
 * Holds if `ast` must have a matching completion, and `e` is the fully converted
 * expression that is being matched in some `switch` statement.
 */
private predicate mustHaveMatchingCompletion(Expr e, AstNode ast) {
  exists(SwitchStmt switch |
    switchMatching(switch, _, ast) and
    e = switch.getExpr().getFullyConverted()
  )
}

/**
 * Holds if `ast` is a (sub-)pattern (or a guard of a top-level pattern) inside
 * case `c`, belonging to `switch` statement `switch`.
 */
private predicate switchMatching(SwitchStmt switch, CaseStmt c, AstNode ast) {
  switch.getACase() = c and
  (
    c.getALabel() = ast
    or
    ast.(Pattern).getImmediateEnclosingPattern+() = c.getALabel().getPattern()
  )
}

/**
 * Holds if `ast` is a (sub-)pattern (or a guard of a top-level pattern) inside
 * case `c`, belonging to `catch` statement `s`.
 */
predicate catchMatching(DoCatchStmt s, CaseStmt c, AstNode ast) {
  catchMatchingCaseLabelItem(s, c, ast)
  or
  catchMatchingPattern(s, c, ast)
}

/**
 * Holds if `cli` a top-level pattern of case `c`, belonging to `catch` statement `s`.
 */
predicate catchMatchingCaseLabelItem(DoCatchStmt s, CaseStmt c, CaseLabelItem cli) {
  s.getACatch() = c and
  c.getALabel() = cli
}

/**
 * Holds if `pattern` is a sub-pattern of the pattern in case
 * statement `c` of the `catch` statement `s`.
 */
predicate catchMatchingPattern(DoCatchStmt s, CaseStmt c, Pattern pattern) {
  s.getACatch() = c and
  exists(CaseLabelItem cli | catchMatching(s, c, cli) |
    cli.getPattern() = pattern
    or
    pattern.getImmediateEnclosingPattern+() = cli.getPattern()
  )
}

/** Gets the value of `e` if it is a constant value, disregarding conversions. */
private string getExprValue(Expr e) {
  result = e.(IntegerLiteralExpr).getStringValue()
  or
  result = e.(BooleanLiteralExpr).getValue().toString()
  or
  result = e.(StringLiteralExpr).getValue()
}

/** Gets the value of `e` if it is a constant value, taking conversions into account. */
private string getConvertedExprValue(Expr e) { result = getExprValue(e.getUnconverted()) }

/** Gets the value of `p` if it is a constant value. */
private string getPatternValue(Pattern p) {
  result = p.(BoolPattern).getValue().toString()
  or
  result = getConvertedExprValue(p.(ExprPattern).getSubExpr())
}

/** Holds if `p` always matches. */
private predicate isIrrefutableMatch(Pattern p) {
  (p instanceof NamedPattern or p instanceof AnyPattern)
  or
  isIrrefutableMatch(p.(TypedPattern).getSubPattern().getFullyUnresolved())
  or
  // A pattern hidden underneath a conversion is also an irrefutable pattern.
  isIrrefutableMatch(p.getResolveStep())
}

/**
 * Holds if the ast node `ast` is a (possibly top-level) pattern that constantly matches (`value = true`) or
 * constantly non-matches (`value = false`).
 */
private predicate isMatchingConstant(AstNode ast, boolean value) {
  isMatchingConstantItem(ast, value)
  or
  isIrrefutableMatch(ast) and
  value = true
}

/**
 * Holds if the top-level pattern `cli` constantly matches (`value = true`) or
 * constantly non-matches (`value = false`).
 */
private predicate isMatchingConstantItem(CaseLabelItem cli, boolean value) {
  // If the pattern always matches
  isIrrefutableMatch(cli.getPattern()) and
  (
    // And there is no guard
    not cli.hasGuard()
    or
    // Or the guard is always true
    getConvertedExprValue(cli.getGuard().getFullyConverted()) = "true"
  ) and
  // Then the pattern always matches
  value = true
  or
  // If the pattern is always false
  getConvertedExprValue(cli.getGuard().getFullyConverted()) = "false" and
  // Then the pattern never matches
  value = false
  or
  // Check if the expression being matched on always matched the pattern
  exists(Expr e, string exprValue, string patternValue |
    mustHaveMatchingCompletion(e, cli) and
    exprValue = getConvertedExprValue(e) and
    patternValue = getPatternValue(cli.getPattern())
  |
    exprValue = patternValue and
    getConvertedExprValue(cli.getGuard()) = "true" and
    value = true
    or
    exprValue != patternValue and
    value = false
    or
    getConvertedExprValue(cli.getGuard()) = "false" and
    value = false
  )
}

private predicate mustHaveThrowCompletion(ThrowStmt throw, ThrowCompletion c) { any() }

private predicate isThrowingType(AnyFunctionType type) { type.isThrowing() }

private predicate mayHaveThrowCompletion(ControlFlowElement n) {
  // An AST expression that may throw.
  isThrowingType(n.asAstNode().(ApplyExpr).getFunction().getType())
  or
  // Getters are the only accessor declarators that may throw.
  exists(Accessor accessor | isThrowingType(accessor.getInterfaceType()) |
    isPropertyGetterElement(n, accessor, _)
  )
}

/**
 * A completion that represents normal evaluation of a statement or an
 * expression.
 */
abstract class NormalCompletion extends Completion {
  override predicate continuesLoop(Stmts::Loops::LoopStmt stmt) { any() }
}

/** A simple (normal) completion. */
class SimpleCompletion extends NormalCompletion, TSimpleCompletion {
  override DirectSuccessor getAMatchingSuccessorType() { any() }

  override string toString() { result = "simple" }
}

/**
 * A completion that represents evaluation of a statement or an
 * expression resulting in a break from a loop.
 */
class BreakCompletion extends TBreakCompletion, Completion {
  Stmt target;

  BreakCompletion() { this = TBreakCompletion(target) }

  override BreakSuccessor getAMatchingSuccessorType() { any() }

  Stmt getTarget() { result = target }

  override string toString() { result = "break" }
}

/**
 * A completion that represents evaluation of a statement or an
 * expression resulting in a continue from a loop.
 */
class ContinueCompletion extends TContinueCompletion, Completion {
  Stmts::Loops::LoopStmt target;

  ContinueCompletion() { this = TContinueCompletion(target) }

  override ContinueSuccessor getAMatchingSuccessorType() { any() }

  override predicate continuesLoop(Stmts::Loops::LoopStmt stmt) { target = stmt }

  Stmts::Loops::LoopStmt getTarget() { result = target }

  override string toString() { result = "continue" }
}

/**
 * A completion that represents a return.
 */
class ReturnCompletion extends TReturnCompletion, Completion {
  override ReturnSuccessor getAMatchingSuccessorType() { any() }

  override string toString() { result = "return" }
}

/**
 * A completion that represents evaluation of an expression, whose value determines
 * the successor. Either a Boolean completion (`BooleanCompletion`), or a matching
 * completion (`MatchingCompletion`).
 */
abstract class ConditionalCompletion extends NormalCompletion {
  boolean value;

  bindingset[value]
  ConditionalCompletion() { any() }

  /** Gets the Boolean value of this conditional completion. */
  final boolean getValue() { result = value }

  /** Gets the dual completion. */
  abstract ConditionalCompletion getDual();
}

/**
 * A completion that represents evaluation of an expression
 * with a Boolean value.
 */
class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
  BooleanCompletion() { this = TBooleanCompletion(value) }

  /** Gets the dual Boolean completion. */
  override BooleanCompletion getDual() { result = TBooleanCompletion(value.booleanNot()) }

  override BooleanSuccessor getAMatchingSuccessorType() { result.getValue() = value }

  override string toString() { result = value.toString() }
}

/** A Boolean `true` completion. */
class TrueCompletion extends BooleanCompletion {
  TrueCompletion() { this.getValue() = true }
}

/** A Boolean `false` completion. */
class FalseCompletion extends BooleanCompletion {
  FalseCompletion() { this.getValue() = false }
}

/**
 * A completion that represents matching, for example a `case` statement in a
 * `switch` statement.
 */
class MatchingCompletion extends ConditionalCompletion, TMatchingCompletion {
  MatchingCompletion() { this = TMatchingCompletion(value) }

  /** Holds if there is a match. */
  predicate isMatch() { value = true }

  /** Holds if there is not a match. */
  predicate isNonMatch() { value = false }

  override MatchingCompletion getDual() { result = TMatchingCompletion(value.booleanNot()) }

  override MatchingSuccessor getAMatchingSuccessorType() { result.getValue() = value }

  override string toString() { if this.isMatch() then result = "match" else result = "no-match" }
}

class FalseOrNonMatchCompletion instanceof ConditionalCompletion {
  FalseOrNonMatchCompletion() {
    this instanceof FalseCompletion
    or
    this.(MatchingCompletion).isNonMatch()
  }

  string toString() {
    result = this.(FalseCompletion).toString()
    or
    result = this.(MatchingCompletion).toString()
  }
}

class TrueOrMatchCompletion instanceof ConditionalCompletion {
  TrueOrMatchCompletion() {
    this instanceof TrueCompletion
    or
    this.(MatchingCompletion).isMatch()
  }

  string toString() {
    result = this.(TrueCompletion).toString()
    or
    result = this.(MatchingCompletion).toString()
  }
}

class FallthroughCompletion extends Completion, TFallthroughCompletion {
  CaseStmt dest;

  FallthroughCompletion() { this = TFallthroughCompletion(dest) }

  override DirectSuccessor getAMatchingSuccessorType() { any() }

  CaseStmt getDestination() { result = dest }

  override string toString() { result = "fallthrough" }
}

/**
 * A completion that represents evaluation of an emptiness test, for example
 * a test in a `foreach` statement.
 */
class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
  EmptinessCompletion() { this = TEmptinessCompletion(value) }

  /** Holds if the emptiness test evaluates to `true`. */
  predicate isEmpty() { value = true }

  override EmptinessCompletion getDual() { result = TEmptinessCompletion(value.booleanNot()) }

  override EmptinessSuccessor getAMatchingSuccessorType() { result.getValue() = value }

  override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" }
}

/** A completion that represents an evaluation that has thrown an exception. */
class ThrowCompletion extends TThrowCompletion, Completion {
  override ExceptionSuccessor getAMatchingSuccessorType() { any() }

  override string toString() { result = "throw" }
}

/**
 * Hold if `c` represents normal evaluation of a statement or an
 * expression.
 */
predicate completionIsNormal(Completion c) { c instanceof NormalCompletion }

/**
 * Hold if `c` represents simple (normal) evaluation of a statement or an
 * expression.
 */
predicate completionIsSimple(Completion c) { c instanceof SimpleCompletion }

/** Holds if `c` is a valid completion for `e`. */
predicate completionIsValidFor(Completion c, ControlFlowElement e) { c.isValidFor(e) }
